pre-p(es; i; ds; a; p; P)
== (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
== c ((alle-at(es;
== c ((alle-at(i;
== c ((alle-at(e.((es-kind(es; e) = locl(a))
== c ((alle-at( (subtype_rel(es-valtype(es; e); p-outcome(p))
== c ((alle-at( c (((P(es-state-when(es; e))))
== c ((alle-at( c  (es-val(es; e) = random{2:n}(p; i; a)(es-kind-index(es; locl(a); e)))))))
== c  alle-at(es;
== c  alle-at(i;
== c  alle-at(e.existse-ge(es;
== c  alle-at(e.existse-ge(e;
== c  alle-at(e.existse-ge(e'.((es-kind(es; e') = locl(a))
== c  alle-at(e.existse-ge( ((t:rationals. (P(es-state-after-elapsed(es; e'; t)))))))))
== c  ((t:rationals. (P(es-init-elapsed(es; i; t))))  (e:es-E(es). (loc(e) = i)))) 

latex

---

clarification:

pre-p(es; i; ds; a; p; P)
== (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
== c ((alle-at(es;
== c ((alle-at(i;
== c ((alle-at(e.((es-kind(es; e) = locl(a)  Knd)
== c ((alle-at( (subtype_rel(es-valtype(es; e); p-outcome(p))
== c ((alle-at( c (((P(es-state-when(es; e))))
== c ((alle-at( c  (es-val(es; e)
== c ((alle-at( c  (=
== c ((alle-at( c  (random{2:n}(p; i; a)(es-kind-index(es; locl(a); e))
== c ((alle-at( c  ( p-outcome(p))))))
== c  alle-at(es;
== c  alle-at(i;
== c  alle-at(e.existse-ge(es;
== c  alle-at(e.existse-ge(e;
== c  alle-at(e.existse-ge(e'.((es-kind(es; e') = locl(a)  Knd)
== c  alle-at(e.existse-ge( ((t:rationals. (P(es-state-after-elapsed(es; e'; t)))))))))
== c  ((t:rationals. (P(es-init-elapsed(es; i; t))))
== c   (e:es-E(es). (es-loc(es; e) = i  Id)))) 

latex

Definitions

es-vartype(es; i; x), fpf-cap(f; eq; x; z), id-deq, top, A c B, es-valtype(es; e), P  Q, es-state-when(es; e), p-outcome(p), es-val(es; e), random{$n:n}(p; a; b), es-kind-index(es; k; e), alle-at(es; i; e.P(e)), existse-ge(es; e; e'.P(e')), P  Q, Knd, es-kind(es; e), locl(a), A, es-state-after-elapsed(es; e; t), P  Q, x:A. B(x), rationals, b, f(a), es-init-elapsed(es; i; t), x:A. B(x), es-E(es), s = t, Id, loc(e)

FDL editor aliases

pre-p